YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Weak Trs:
  { #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We add following dependency tuples:

Strict DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , findMin^#(@l) -> c_2(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs))
  , minSort#1^#(nil()) -> c_11() }
Weak DPs:
  { #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x))
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y))
  , #compare^#(#s(@x), #0()) -> c_22()
  , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , findMin^#(@l) -> c_2(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs))
  , minSort#1^#(nil()) -> c_11() }
Weak DPs:
  { #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x))
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y))
  , #compare^#(#s(@x), #0()) -> c_22()
  , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We estimate the number of application of {1,4,6,7,8,11} by
applications of Pre({1,4,6,7,8,11}) = {2,3,5,9}. Here rules are
labeled as follows:

  DPs:
    { 1: #less^#(@x, @y) ->
         c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
    , 2: findMin^#(@l) -> c_2(findMin#1^#(@l))
    , 3: findMin#1^#(::(@x, @xs)) ->
         c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
    , 4: findMin#1^#(nil()) -> c_4()
    , 5: findMin#2^#(::(@y, @ys), @x) ->
         c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
    , 6: findMin#2^#(nil(), @x) -> c_6()
    , 7: findMin#3^#(#false(), @x, @y, @ys) -> c_7()
    , 8: findMin#3^#(#true(), @x, @y, @ys) -> c_8()
    , 9: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
    , 10: minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs))
    , 11: minSort#1^#(nil()) -> c_11()
    , 12: #cklt^#(#EQ()) -> c_24()
    , 13: #cklt^#(#GT()) -> c_25()
    , 14: #cklt^#(#LT()) -> c_26()
    , 15: #compare^#(#0(), #0()) -> c_12()
    , 16: #compare^#(#0(), #neg(@y)) -> c_13()
    , 17: #compare^#(#0(), #pos(@y)) -> c_14()
    , 18: #compare^#(#0(), #s(@y)) -> c_15()
    , 19: #compare^#(#neg(@x), #0()) -> c_16()
    , 20: #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x))
    , 21: #compare^#(#neg(@x), #pos(@y)) -> c_18()
    , 22: #compare^#(#pos(@x), #0()) -> c_19()
    , 23: #compare^#(#pos(@x), #neg(@y)) -> c_20()
    , 24: #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y))
    , 25: #compare^#(#s(@x), #0()) -> c_22()
    , 26: #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> c_2(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) }
Weak DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x))
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y))
  , #compare^#(#s(@x), #0()) -> c_22()
  , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y))
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort#1^#(nil()) -> c_11() }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We estimate the number of application of {3} by applications of
Pre({3}) = {2}. Here rules are labeled as follows:

  DPs:
    { 1: findMin^#(@l) -> c_2(findMin#1^#(@l))
    , 2: findMin#1^#(::(@x, @xs)) ->
         c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
    , 3: findMin#2^#(::(@y, @ys), @x) ->
         c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
    , 4: minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
    , 5: minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs))
    , 6: #less^#(@x, @y) ->
         c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
    , 7: #cklt^#(#EQ()) -> c_24()
    , 8: #cklt^#(#GT()) -> c_25()
    , 9: #cklt^#(#LT()) -> c_26()
    , 10: #compare^#(#0(), #0()) -> c_12()
    , 11: #compare^#(#0(), #neg(@y)) -> c_13()
    , 12: #compare^#(#0(), #pos(@y)) -> c_14()
    , 13: #compare^#(#0(), #s(@y)) -> c_15()
    , 14: #compare^#(#neg(@x), #0()) -> c_16()
    , 15: #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x))
    , 16: #compare^#(#neg(@x), #pos(@y)) -> c_18()
    , 17: #compare^#(#pos(@x), #0()) -> c_19()
    , 18: #compare^#(#pos(@x), #neg(@y)) -> c_20()
    , 19: #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y))
    , 20: #compare^#(#s(@x), #0()) -> c_22()
    , 21: #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y))
    , 22: findMin#1^#(nil()) -> c_4()
    , 23: findMin#2^#(nil(), @x) -> c_6()
    , 24: findMin#3^#(#false(), @x, @y, @ys) -> c_7()
    , 25: findMin#3^#(#true(), @x, @y, @ys) -> c_8()
    , 26: minSort#1^#(nil()) -> c_11() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> c_2(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) }
Weak DPs:
  { #less^#(@x, @y) ->
    c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
  , #cklt^#(#EQ()) -> c_24()
  , #cklt^#(#GT()) -> c_25()
  , #cklt^#(#LT()) -> c_26()
  , #compare^#(#0(), #0()) -> c_12()
  , #compare^#(#0(), #neg(@y)) -> c_13()
  , #compare^#(#0(), #pos(@y)) -> c_14()
  , #compare^#(#0(), #s(@y)) -> c_15()
  , #compare^#(#neg(@x), #0()) -> c_16()
  , #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x))
  , #compare^#(#neg(@x), #pos(@y)) -> c_18()
  , #compare^#(#pos(@x), #0()) -> c_19()
  , #compare^#(#pos(@x), #neg(@y)) -> c_20()
  , #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y))
  , #compare^#(#s(@x), #0()) -> c_22()
  , #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y))
  , findMin#1^#(nil()) -> c_4()
  , findMin#2^#(::(@y, @ys), @x) ->
    c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
  , findMin#2^#(nil(), @x) -> c_6()
  , findMin#3^#(#false(), @x, @y, @ys) -> c_7()
  , findMin#3^#(#true(), @x, @y, @ys) -> c_8()
  , minSort#1^#(nil()) -> c_11() }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ #less^#(@x, @y) ->
  c_1(#cklt^#(#compare(@x, @y)), #compare^#(@x, @y))
, #cklt^#(#EQ()) -> c_24()
, #cklt^#(#GT()) -> c_25()
, #cklt^#(#LT()) -> c_26()
, #compare^#(#0(), #0()) -> c_12()
, #compare^#(#0(), #neg(@y)) -> c_13()
, #compare^#(#0(), #pos(@y)) -> c_14()
, #compare^#(#0(), #s(@y)) -> c_15()
, #compare^#(#neg(@x), #0()) -> c_16()
, #compare^#(#neg(@x), #neg(@y)) -> c_17(#compare^#(@y, @x))
, #compare^#(#neg(@x), #pos(@y)) -> c_18()
, #compare^#(#pos(@x), #0()) -> c_19()
, #compare^#(#pos(@x), #neg(@y)) -> c_20()
, #compare^#(#pos(@x), #pos(@y)) -> c_21(#compare^#(@x, @y))
, #compare^#(#s(@x), #0()) -> c_22()
, #compare^#(#s(@x), #s(@y)) -> c_23(#compare^#(@x, @y))
, findMin#1^#(nil()) -> c_4()
, findMin#2^#(::(@y, @ys), @x) ->
  c_5(findMin#3^#(#less(@x, @y), @x, @y, @ys), #less^#(@x, @y))
, findMin#2^#(nil(), @x) -> c_6()
, findMin#3^#(#false(), @x, @y, @ys) -> c_7()
, findMin#3^#(#true(), @x, @y, @ys) -> c_8()
, minSort#1^#(nil()) -> c_11() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> c_2(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs))
  , minSort^#(@l) -> c_9(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_10(minSort^#(@xs)) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { findMin#1^#(::(@x, @xs)) ->
    c_3(findMin#2^#(findMin(@xs), @x), findMin^#(@xs)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> c_1(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs))
  , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
  , minSort(@l) -> minSort#1(findMin(@l))
  , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
  , minSort#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { #less(@x, @y) -> #cklt(#compare(@x, @y))
    , #compare(#0(), #0()) -> #EQ()
    , #compare(#0(), #neg(@y)) -> #GT()
    , #compare(#0(), #pos(@y)) -> #LT()
    , #compare(#0(), #s(@y)) -> #LT()
    , #compare(#neg(@x), #0()) -> #LT()
    , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
    , #compare(#neg(@x), #pos(@y)) -> #LT()
    , #compare(#pos(@x), #0()) -> #GT()
    , #compare(#pos(@x), #neg(@y)) -> #GT()
    , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
    , #compare(#s(@x), #0()) -> #GT()
    , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
    , #cklt(#EQ()) -> #false()
    , #cklt(#GT()) -> #false()
    , #cklt(#LT()) -> #true()
    , findMin(@l) -> findMin#1(@l)
    , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
    , findMin#1(nil()) -> nil()
    , findMin#2(::(@y, @ys), @x) ->
      findMin#3(#less(@x, @y), @x, @y, @ys)
    , findMin#2(nil(), @x) -> ::(@x, nil())
    , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
    , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> c_1(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs))
  , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.

DPs:
  { 2: findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) }
Trs:
  { #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false() }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
    Uargs(c_4) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
                  [#less](x1, x2) = [2 0] x1 + [2 0] x2 + [2]
                                    [0 0]      [0 0]      [0]
                                                             
               [#compare](x1, x2) = [0 1] x1 + [0 1] x2 + [0]
                                    [1 0]      [1 0]      [1]
                                                             
                      [#cklt](x1) = [0 2] x1 + [0]
                                    [0 0]      [0]
                                                  
                    [findMin](x1) = [1 0] x1 + [0]
                                    [0 1]      [0]
                                                  
                  [findMin#1](x1) = [1 0] x1 + [0]
                                    [0 1]      [0]
                                                  
                     [::](x1, x2) = [1 0] x2 + [1]
                                    [1 1]      [0]
                                                  
              [findMin#2](x1, x2) = [1 0] x1 + [1]
                                    [1 1]      [0]
                                                  
                            [nil] = [0]
                                    [1]
                                       
      [findMin#3](x1, x2, x3, x4) = [0 1] x1 + [1 0] x4 + [2]
                                    [0 0]      [2 1]      [1]
                                                             
                         [#false] = [1]
                                    [0]
                                       
                          [#true] = [2]
                                    [0]
                                       
                    [minSort](x1) = [0]
                                    [0]
                                       
                  [minSort#1](x1) = [0]
                                    [0]
                                       
                            [#EQ] = [0]
                                    [1]
                                       
                            [#GT] = [1]
                                    [2]
                                       
                            [#LT] = [0]
                                    [1]
                                       
                             [#0] = [2]
                                    [0]
                                       
                       [#neg](x1) = [1 0] x1 + [1]
                                    [1 1]      [2]
                                                  
                       [#pos](x1) = [1 0] x1 + [0]
                                    [0 1]      [2]
                                                  
                         [#s](x1) = [1 0] x1 + [0]
                                    [1 1]      [1]
                                                  
                [#less^#](x1, x2) = [0]
                                    [0]
                                       
                    [c_1](x1, x2) = [0]
                                    [0]
                                       
                    [#cklt^#](x1) = [0]
                                    [0]
                                       
             [#compare^#](x1, x2) = [0]
                                    [0]
                                       
                  [findMin^#](x1) = [2 0] x1 + [0]
                                    [0 0]      [0]
                                                  
                        [c_2](x1) = [0]
                                    [0]
                                       
                [findMin#1^#](x1) = [2 0] x1 + [0]
                                    [0 0]      [0]
                                                  
                    [c_3](x1, x2) = [0]
                                    [0]
                                       
            [findMin#2^#](x1, x2) = [0]
                                    [0]
                                       
                            [c_4] = [0]
                                    [0]
                                       
                    [c_5](x1, x2) = [0]
                                    [0]
                                       
    [findMin#3^#](x1, x2, x3, x4) = [0]
                                    [0]
                                       
                            [c_6] = [0]
                                    [0]
                                       
                            [c_7] = [0]
                                    [0]
                                       
                            [c_8] = [0]
                                    [0]
                                       
                  [minSort^#](x1) = [2 2] x1 + [2]
                                    [1 1]      [0]
                                                  
                    [c_9](x1, x2) = [0]
                                    [0]
                                       
                [minSort#1^#](x1) = [0 2] x1 + [2]
                                    [0 0]      [0]
                                                  
                       [c_10](x1) = [0]
                                    [0]
                                       
                           [c_11] = [0]
                                    [0]
                                       
                           [c_12] = [0]
                                    [0]
                                       
                           [c_13] = [0]
                                    [0]
                                       
                           [c_14] = [0]
                                    [0]
                                       
                           [c_15] = [0]
                                    [0]
                                       
                           [c_16] = [0]
                                    [0]
                                       
                       [c_17](x1) = [0]
                                    [0]
                                       
                           [c_18] = [0]
                                    [0]
                                       
                           [c_19] = [0]
                                    [0]
                                       
                           [c_20] = [0]
                                    [0]
                                       
                       [c_21](x1) = [0]
                                    [0]
                                       
                           [c_22] = [0]
                                    [0]
                                       
                       [c_23](x1) = [0]
                                    [0]
                                       
                           [c_24] = [0]
                                    [0]
                                       
                           [c_25] = [0]
                                    [0]
                                       
                           [c_26] = [0]
                                    [0]
                                       
                              [c] = [0]
                                    [0]
                                       
                        [c_1](x1) = [1 1] x1 + [0]
                                    [0 0]      [0]
                                                  
                        [c_2](x1) = [1 1] x1 + [0]
                                    [0 0]      [0]
                                                  
                    [c_3](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
                                    [0 0]      [0 0]      [0]
                                                             
                        [c_4](x1) = [1 0] x1 + [0]
                                    [0 0]      [0]
  
  This order satisfies following ordering constraints
  
                       [#less(@x, @y)] =  [2 0] @x + [2 0] @y + [2]                     
                                          [0 0]      [0 0]      [0]                     
                                       >= [2 0] @x + [2 0] @y + [2]                     
                                          [0 0]      [0 0]      [0]                     
                                       =  [#cklt(#compare(@x, @y))]                     
                                                                                        
                [#compare(#0(), #0())] =  [0]                                           
                                          [5]                                           
                                       >= [0]                                           
                                          [1]                                           
                                       =  [#EQ()]                                       
                                                                                        
            [#compare(#0(), #neg(@y))] =  [1 1] @y + [2]                                
                                          [1 0]      [4]                                
                                       >  [1]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
            [#compare(#0(), #pos(@y))] =  [0 1] @y + [2]                                
                                          [1 0]      [3]                                
                                       >  [0]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
              [#compare(#0(), #s(@y))] =  [1 1] @y + [1]                                
                                          [1 0]      [3]                                
                                       >  [0]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
            [#compare(#neg(@x), #0())] =  [1 1] @x + [2]                                
                                          [1 0]      [4]                                
                                       >  [0]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
        [#compare(#neg(@x), #neg(@y))] =  [1 1] @x + [1 1] @y + [4]                     
                                          [1 0]      [1 0]      [3]                     
                                       >  [0 1] @x + [0 1] @y + [0]                     
                                          [1 0]      [1 0]      [1]                     
                                       =  [#compare(@y, @x)]                            
                                                                                        
        [#compare(#neg(@x), #pos(@y))] =  [1 1] @x + [0 1] @y + [4]                     
                                          [1 0]      [1 0]      [2]                     
                                       >  [0]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
            [#compare(#pos(@x), #0())] =  [0 1] @x + [2]                                
                                          [1 0]      [3]                                
                                       >  [1]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
        [#compare(#pos(@x), #neg(@y))] =  [0 1] @x + [1 1] @y + [4]                     
                                          [1 0]      [1 0]      [2]                     
                                       >  [1]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
        [#compare(#pos(@x), #pos(@y))] =  [0 1] @x + [0 1] @y + [4]                     
                                          [1 0]      [1 0]      [1]                     
                                       >  [0 1] @x + [0 1] @y + [0]                     
                                          [1 0]      [1 0]      [1]                     
                                       =  [#compare(@x, @y)]                            
                                                                                        
              [#compare(#s(@x), #0())] =  [1 1] @x + [1]                                
                                          [1 0]      [3]                                
                                       >= [1]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
            [#compare(#s(@x), #s(@y))] =  [1 1] @x + [1 1] @y + [2]                     
                                          [1 0]      [1 0]      [1]                     
                                       >  [0 1] @x + [0 1] @y + [0]                     
                                          [1 0]      [1 0]      [1]                     
                                       =  [#compare(@x, @y)]                            
                                                                                        
                        [#cklt(#EQ())] =  [2]                                           
                                          [0]                                           
                                       >  [1]                                           
                                          [0]                                           
                                       =  [#false()]                                    
                                                                                        
                        [#cklt(#GT())] =  [4]                                           
                                          [0]                                           
                                       >  [1]                                           
                                          [0]                                           
                                       =  [#false()]                                    
                                                                                        
                        [#cklt(#LT())] =  [2]                                           
                                          [0]                                           
                                       >= [2]                                           
                                          [0]                                           
                                       =  [#true()]                                     
                                                                                        
                         [findMin(@l)] =  [1 0] @l + [0]                                
                                          [0 1]      [0]                                
                                       >= [1 0] @l + [0]                                
                                          [0 1]      [0]                                
                                       =  [findMin#1(@l)]                               
                                                                                        
              [findMin#1(::(@x, @xs))] =  [1 0] @xs + [1]                               
                                          [1 1]       [0]                               
                                       >= [1 0] @xs + [1]                               
                                          [1 1]       [0]                               
                                       =  [findMin#2(findMin(@xs), @x)]                 
                                                                                        
                    [findMin#1(nil())] =  [0]                                           
                                          [1]                                           
                                       >= [0]                                           
                                          [1]                                           
                                       =  [nil()]                                       
                                                                                        
          [findMin#2(::(@y, @ys), @x)] =  [1 0] @ys + [2]                               
                                          [2 1]       [1]                               
                                       >= [1 0] @ys + [2]                               
                                          [2 1]       [1]                               
                                       =  [findMin#3(#less(@x, @y), @x, @y, @ys)]       
                                                                                        
                [findMin#2(nil(), @x)] =  [1]                                           
                                          [1]                                           
                                       >= [1]                                           
                                          [1]                                           
                                       =  [::(@x, nil())]                               
                                                                                        
    [findMin#3(#false(), @x, @y, @ys)] =  [1 0] @ys + [2]                               
                                          [2 1]       [1]                               
                                       >= [1 0] @ys + [2]                               
                                          [2 1]       [1]                               
                                       =  [::(@y, ::(@x, @ys))]                         
                                                                                        
     [findMin#3(#true(), @x, @y, @ys)] =  [1 0] @ys + [2]                               
                                          [2 1]       [1]                               
                                       >= [1 0] @ys + [2]                               
                                          [2 1]       [1]                               
                                       =  [::(@x, ::(@y, @ys))]                         
                                                                                        
                       [findMin^#(@l)] =  [2 0] @l + [0]                                
                                          [0 0]      [0]                                
                                       >= [2 0] @l + [0]                                
                                          [0 0]      [0]                                
                                       =  [c_1(findMin#1^#(@l))]                        
                                                                                        
            [findMin#1^#(::(@x, @xs))] =  [2 0] @xs + [2]                               
                                          [0 0]       [0]                               
                                       >  [2 0] @xs + [0]                               
                                          [0 0]       [0]                               
                                       =  [c_2(findMin^#(@xs))]                         
                                                                                        
                       [minSort^#(@l)] =  [2 2] @l + [2]                                
                                          [1 1]      [0]                                
                                       >= [2 2] @l + [2]                                
                                          [0 0]      [0]                                
                                       =  [c_3(minSort#1^#(findMin(@l)), findMin^#(@l))]
                                                                                        
            [minSort#1^#(::(@x, @xs))] =  [2 2] @xs + [2]                               
                                          [0 0]       [0]                               
                                       >= [2 2] @xs + [2]                               
                                          [0 0]       [0]                               
                                       =  [c_4(minSort^#(@xs))]                         
                                                                                        

The strictly oriented rules are moved into the corresponding weak
component(s).


We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict DPs:
  { findMin^#(@l) -> c_1(findMin#1^#(@l))
  , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) }
Weak DPs: { findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.

DPs:
  { 3: minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs))
  , 4: findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) }
Trs:
  { #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT() }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
    Uargs(c_4) = {1}
  
  TcT has computed following constructor-based matrix interpretation
  satisfying not(EDA).
  
                  [#less](x1, x2) = [2]
                                    [1]
                                       
               [#compare](x1, x2) = [2 2] x1 + [2 2] x2 + [0]
                                    [1 1]      [1 1]      [1]
                                                             
                      [#cklt](x1) = [2]
                                    [1]
                                       
                    [findMin](x1) = [1 0] x1 + [0]
                                    [0 1]      [2]
                                                  
                  [findMin#1](x1) = [1 0] x1 + [0]
                                    [0 1]      [2]
                                                  
                     [::](x1, x2) = [1 0] x2 + [1]
                                    [1 1]      [2]
                                                  
              [findMin#2](x1, x2) = [1 0] x1 + [1]
                                    [1 1]      [2]
                                                  
                            [nil] = [0]
                                    [2]
                                       
      [findMin#3](x1, x2, x3, x4) = [0 1] x1 + [1 0] x4 + [1]
                                    [1 1]      [2 1]      [2]
                                                             
                         [#false] = [2]
                                    [1]
                                       
                          [#true] = [2]
                                    [1]
                                       
                    [minSort](x1) = [0]
                                    [0]
                                       
                  [minSort#1](x1) = [0]
                                    [0]
                                       
                            [#EQ] = [0]
                                    [2]
                                       
                            [#GT] = [0]
                                    [2]
                                       
                            [#LT] = [1]
                                    [1]
                                       
                             [#0] = [1]
                                    [0]
                                       
                       [#neg](x1) = [1 0] x1 + [0]
                                    [0 1]      [1]
                                                  
                       [#pos](x1) = [1 0] x1 + [1]
                                    [0 1]      [0]
                                                  
                         [#s](x1) = [1 0] x1 + [0]
                                    [0 1]      [0]
                                                  
                [#less^#](x1, x2) = [0]
                                    [0]
                                       
                    [c_1](x1, x2) = [0]
                                    [0]
                                       
                    [#cklt^#](x1) = [0]
                                    [0]
                                       
             [#compare^#](x1, x2) = [0]
                                    [0]
                                       
                  [findMin^#](x1) = [1 0] x1 + [0]
                                    [0 0]      [1]
                                                  
                        [c_2](x1) = [0]
                                    [0]
                                       
                [findMin#1^#](x1) = [1 0] x1 + [0]
                                    [0 0]      [1]
                                                  
                    [c_3](x1, x2) = [0]
                                    [0]
                                       
            [findMin#2^#](x1, x2) = [0]
                                    [0]
                                       
                            [c_4] = [0]
                                    [0]
                                       
                    [c_5](x1, x2) = [0]
                                    [0]
                                       
    [findMin#3^#](x1, x2, x3, x4) = [0]
                                    [0]
                                       
                            [c_6] = [0]
                                    [0]
                                       
                            [c_7] = [0]
                                    [0]
                                       
                            [c_8] = [0]
                                    [0]
                                       
                  [minSort^#](x1) = [2 1] x1 + [2]
                                    [0 0]      [0]
                                                  
                    [c_9](x1, x2) = [0]
                                    [0]
                                       
                [minSort#1^#](x1) = [1 1] x1 + [0]
                                    [0 0]      [0]
                                                  
                       [c_10](x1) = [0]
                                    [0]
                                       
                           [c_11] = [0]
                                    [0]
                                       
                           [c_12] = [0]
                                    [0]
                                       
                           [c_13] = [0]
                                    [0]
                                       
                           [c_14] = [0]
                                    [0]
                                       
                           [c_15] = [0]
                                    [0]
                                       
                           [c_16] = [0]
                                    [0]
                                       
                       [c_17](x1) = [0]
                                    [0]
                                       
                           [c_18] = [0]
                                    [0]
                                       
                           [c_19] = [0]
                                    [0]
                                       
                           [c_20] = [0]
                                    [0]
                                       
                       [c_21](x1) = [0]
                                    [0]
                                       
                           [c_22] = [0]
                                    [0]
                                       
                       [c_23](x1) = [0]
                                    [0]
                                       
                           [c_24] = [0]
                                    [0]
                                       
                           [c_25] = [0]
                                    [0]
                                       
                           [c_26] = [0]
                                    [0]
                                       
                              [c] = [0]
                                    [0]
                                       
                        [c_1](x1) = [1 0] x1 + [0]
                                    [0 0]      [0]
                                                  
                        [c_2](x1) = [1 0] x1 + [0]
                                    [0 0]      [0]
                                                  
                    [c_3](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
                                    [0 0]      [0 0]      [0]
                                                             
                        [c_4](x1) = [1 1] x1 + [0]
                                    [0 0]      [0]
  
  This order satisfies following ordering constraints
  
                       [#less(@x, @y)] =  [2]                                           
                                          [1]                                           
                                       >= [2]                                           
                                          [1]                                           
                                       =  [#cklt(#compare(@x, @y))]                     
                                                                                        
                [#compare(#0(), #0())] =  [4]                                           
                                          [3]                                           
                                       >  [0]                                           
                                          [2]                                           
                                       =  [#EQ()]                                       
                                                                                        
            [#compare(#0(), #neg(@y))] =  [2 2] @y + [4]                                
                                          [1 1]      [3]                                
                                       >  [0]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
            [#compare(#0(), #pos(@y))] =  [2 2] @y + [4]                                
                                          [1 1]      [3]                                
                                       >  [1]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
              [#compare(#0(), #s(@y))] =  [2 2] @y + [2]                                
                                          [1 1]      [2]                                
                                       >  [1]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
            [#compare(#neg(@x), #0())] =  [2 2] @x + [4]                                
                                          [1 1]      [3]                                
                                       >  [1]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
        [#compare(#neg(@x), #neg(@y))] =  [2 2] @x + [2 2] @y + [4]                     
                                          [1 1]      [1 1]      [3]                     
                                       >  [2 2] @x + [2 2] @y + [0]                     
                                          [1 1]      [1 1]      [1]                     
                                       =  [#compare(@y, @x)]                            
                                                                                        
        [#compare(#neg(@x), #pos(@y))] =  [2 2] @x + [2 2] @y + [4]                     
                                          [1 1]      [1 1]      [3]                     
                                       >  [1]                                           
                                          [1]                                           
                                       =  [#LT()]                                       
                                                                                        
            [#compare(#pos(@x), #0())] =  [2 2] @x + [4]                                
                                          [1 1]      [3]                                
                                       >  [0]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
        [#compare(#pos(@x), #neg(@y))] =  [2 2] @x + [2 2] @y + [4]                     
                                          [1 1]      [1 1]      [3]                     
                                       >  [0]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
        [#compare(#pos(@x), #pos(@y))] =  [2 2] @x + [2 2] @y + [4]                     
                                          [1 1]      [1 1]      [3]                     
                                       >  [2 2] @x + [2 2] @y + [0]                     
                                          [1 1]      [1 1]      [1]                     
                                       =  [#compare(@x, @y)]                            
                                                                                        
              [#compare(#s(@x), #0())] =  [2 2] @x + [2]                                
                                          [1 1]      [2]                                
                                       >  [0]                                           
                                          [2]                                           
                                       =  [#GT()]                                       
                                                                                        
            [#compare(#s(@x), #s(@y))] =  [2 2] @x + [2 2] @y + [0]                     
                                          [1 1]      [1 1]      [1]                     
                                       >= [2 2] @x + [2 2] @y + [0]                     
                                          [1 1]      [1 1]      [1]                     
                                       =  [#compare(@x, @y)]                            
                                                                                        
                        [#cklt(#EQ())] =  [2]                                           
                                          [1]                                           
                                       >= [2]                                           
                                          [1]                                           
                                       =  [#false()]                                    
                                                                                        
                        [#cklt(#GT())] =  [2]                                           
                                          [1]                                           
                                       >= [2]                                           
                                          [1]                                           
                                       =  [#false()]                                    
                                                                                        
                        [#cklt(#LT())] =  [2]                                           
                                          [1]                                           
                                       >= [2]                                           
                                          [1]                                           
                                       =  [#true()]                                     
                                                                                        
                         [findMin(@l)] =  [1 0] @l + [0]                                
                                          [0 1]      [2]                                
                                       >= [1 0] @l + [0]                                
                                          [0 1]      [2]                                
                                       =  [findMin#1(@l)]                               
                                                                                        
              [findMin#1(::(@x, @xs))] =  [1 0] @xs + [1]                               
                                          [1 1]       [4]                               
                                       >= [1 0] @xs + [1]                               
                                          [1 1]       [4]                               
                                       =  [findMin#2(findMin(@xs), @x)]                 
                                                                                        
                    [findMin#1(nil())] =  [0]                                           
                                          [4]                                           
                                       >= [0]                                           
                                          [2]                                           
                                       =  [nil()]                                       
                                                                                        
          [findMin#2(::(@y, @ys), @x)] =  [1 0] @ys + [2]                               
                                          [2 1]       [5]                               
                                       >= [1 0] @ys + [2]                               
                                          [2 1]       [5]                               
                                       =  [findMin#3(#less(@x, @y), @x, @y, @ys)]       
                                                                                        
                [findMin#2(nil(), @x)] =  [1]                                           
                                          [4]                                           
                                       >= [1]                                           
                                          [4]                                           
                                       =  [::(@x, nil())]                               
                                                                                        
    [findMin#3(#false(), @x, @y, @ys)] =  [1 0] @ys + [2]                               
                                          [2 1]       [5]                               
                                       >= [1 0] @ys + [2]                               
                                          [2 1]       [5]                               
                                       =  [::(@y, ::(@x, @ys))]                         
                                                                                        
     [findMin#3(#true(), @x, @y, @ys)] =  [1 0] @ys + [2]                               
                                          [2 1]       [5]                               
                                       >= [1 0] @ys + [2]                               
                                          [2 1]       [5]                               
                                       =  [::(@x, ::(@y, @ys))]                         
                                                                                        
                       [findMin^#(@l)] =  [1 0] @l + [0]                                
                                          [0 0]      [1]                                
                                       >= [1 0] @l + [0]                                
                                          [0 0]      [0]                                
                                       =  [c_1(findMin#1^#(@l))]                        
                                                                                        
            [findMin#1^#(::(@x, @xs))] =  [1 0] @xs + [1]                               
                                          [0 0]       [1]                               
                                       >  [1 0] @xs + [0]                               
                                          [0 0]       [0]                               
                                       =  [c_2(findMin^#(@xs))]                         
                                                                                        
                       [minSort^#(@l)] =  [2 1] @l + [2]                                
                                          [0 0]      [0]                                
                                       >= [2 1] @l + [2]                                
                                          [0 0]      [0]                                
                                       =  [c_3(minSort#1^#(findMin(@l)), findMin^#(@l))]
                                                                                        
            [minSort#1^#(::(@x, @xs))] =  [2 1] @xs + [3]                               
                                          [0 0]       [0]                               
                                       >  [2 1] @xs + [2]                               
                                          [0 0]       [0]                               
                                       =  [c_4(minSort^#(@xs))]                         
                                                                                        

Consider the set of all dependency pairs

DPs:
  { 1: findMin^#(@l) -> c_1(findMin#1^#(@l))
  , 2: minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l))
  , 3: minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs))
  , 4: findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs)) }

Processor 'matrix interpretation of dimension 2' induces the
complexity certificate YES(?,O(n^2)) on application of dependency
pairs {3,4}. These cover all (indirect) predecessors of dependency
pairs {1,2,3,4}, their number of application is equally bounded.
The dependency pairs are shifted into the corresponding weak
component(s).

We apply the transformation 'removetails' on the sub-problem:

Weak DPs:
  { findMin^#(@l) -> c_1(findMin#1^#(@l))
  , findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs))
  , minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l))
  , minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) }
Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
StartTerms: basic terms
Strategy: innermost

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ findMin^#(@l) -> c_1(findMin#1^#(@l))
, findMin#1^#(::(@x, @xs)) -> c_2(findMin^#(@xs))
, minSort^#(@l) -> c_3(minSort#1^#(findMin(@l)), findMin^#(@l))
, minSort#1^#(::(@x, @xs)) -> c_4(minSort^#(@xs)) }


We apply the transformation 'usablerules' on the sub-problem:

Weak Trs:
  { #less(@x, @y) -> #cklt(#compare(@x, @y))
  , #compare(#0(), #0()) -> #EQ()
  , #compare(#0(), #neg(@y)) -> #GT()
  , #compare(#0(), #pos(@y)) -> #LT()
  , #compare(#0(), #s(@y)) -> #LT()
  , #compare(#neg(@x), #0()) -> #LT()
  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
  , #compare(#neg(@x), #pos(@y)) -> #LT()
  , #compare(#pos(@x), #0()) -> #GT()
  , #compare(#pos(@x), #neg(@y)) -> #GT()
  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
  , #compare(#s(@x), #0()) -> #GT()
  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)
  , #cklt(#EQ()) -> #false()
  , #cklt(#GT()) -> #false()
  , #cklt(#LT()) -> #true()
  , findMin(@l) -> findMin#1(@l)
  , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
  , findMin#1(nil()) -> nil()
  , findMin#2(::(@y, @ys), @x) ->
    findMin#3(#less(@x, @y), @x, @y, @ys)
  , findMin#2(nil(), @x) -> ::(@x, nil())
  , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
  , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) }
StartTerms: basic terms
Strategy: innermost

No rule is usable, rules are removed from the input problem.


We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^2))